A:MsgA, x, z:Id, k:Knd, s1, s2:A.state, v:A.da(k).
ma-frame-compat(A;A)
 A.rframe(k reads x)
 (s1  s2 mod x)
 z = x
 A.ef(k,z,s1,v)?s1(z) = A.ef(k,z,s2,v)?s2(z)  A.ds(z) 

latex

Definitions

t  T, IdDeq, x:A. B(x), P  Q, Id, Type, Void, f(x)?z, Top, f(a), x.A(x), nat-deq-aux, NatDeq, atom-deq-aux, AtomDeq, #$n, a<b, False, x:AB(x), A, AB, , {x:A| B(x) }, , Atom, prod-deq(A;B;a;b), proddeq(a;b), product-deq(A;B;a;b), Knd, 2of(t), KindDeq, x:AB(x), x. t(x), 1of(t), f(x), s = t, Prop, M.ds(x), (s1  s2 mod x), a:A fp B(a), x:A. B(x), inl(x), left+right, Case b of inl(x)  s(x) ; inr(y)  t(y), if b t else f fi, type List, x  dom(f), b, P  Q, S  T, Dec(P), P & Q, IdLnk, b, , P  Q, Unit, M.ef(k,x,s,v)?w, State(ds), xdom(f). v=f(x)   P(x;v), M.da(a), M.state, z != f(x)  P(a;z), M.rframe(A.sends tfL of k on l), M.sframe(k sends <l,tg>), M.rframe(A.effect f of k on y), M.aframe(k affects x), M.frame(k affects x), M.rframe(A.pre p for a), ma-frame-compat(A;B), Valtype(da;k), M.rframe(k reads x), MsgA, <a,b>

Lemmas

ma-x-equiv wf, ma-rframe wf, ma-frame-compat wf, ma-da wf, ma-st wf, msga wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bool wf, bnot wf, not wf, decidable assert, assert wf, fpf-dom wf, fpf-trivial-subtype-top, fpf-ap wf, pi1 wf, top wf, fpf-cap wf, pi2 wf, product-deq wf, Knd wf, Kind-deq wf, fpf-cap-void-subtype, Id wf, id-deq wf